A:Type, B, eq, g:Top.   g 

latex

Definitions	x:A. B(x), f  g, , P  Q, b, x  dom(f), A c B, deq-member(eq;x;L), t.1, reduce(f;k;as), ff, Y, if b then t else f fi , t  T, False,
Lemmas	false wf, top wf